T:Type, R:(TT), x, y:T. (x R^+ y)  ((x R y)  (z:T. ((x R z) & (z R^+ y)))) 

latex

Definitions	Type, , Dec(P), s ~ t, s = t, SQType(T), {T}, , #$n, P  Q, left + right, x:A. B(x), P & Q, x:A  B(x), R^+, x f y, f(a), rel_exp(T;R;n), , {x:A| B(x)} , A, False, x:AB(x), Void, A  B, x:A. B(x), P  Q, t  T, , a < b, (i = j), Unit, P  Q, , b, b, n - m, n+m, if b then t else f fi , x.A(x), T, True
Lemmas	nat plus inc, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, le wf, rel exp wf, decidable int equal, nat plus properties, rel plus wf